A:Type, op:(AAA), id:A, p:, q:{p...}, E:({p..q}A). (op,id) p  i < q. E(i)  A 

latex

Up	groups 1
Definitions	A  B, A, False, P  Q, {i..j}, {x:A| B(x)} , {i...}, x:A. B(x), , x:AB(x), t  T, Type, x.A(x), n - m, , !Void(), n+m, -n, #$n, i  j , a < b, (op,id) lb  i < ub. E(i), x. t(x), x(s), f(a), , s = t
Lemmas	nat wf, itop wf, nat properties, ge wf, le wf, int upper wf, int seg wf